\section{Future work}
\label{sec:future}

Zeno has been developed to explore only fully automated proof techniques for Haskell style functional programs. Although we have had reasonable success in this area the tools we are comparing it to are far more advanced in many other ways. 

IsaPlanner is a rippling based tool which uses this very advanced heuristic to guide the application of background lemmas. Zeno does not support any background lemmas aside from function definitions and we would need to integrate a technique such as rippling into our existing work to allow for these. IsaPlanner is also more generally a proof-planner for the Isabelle system, allowing it to be used within larger, human guided proofs, and ensuring any generated proofs are sound. Integration into a proof system like Isabelle, perhaps as a tactic for IsaPlanner, would be necessary for Zeno to become a useful tool to the software verification community.

ACL2s is an industrial strength theorem proving environment which has been used for the verification of important properties of real-world systems. It can also prove properties over full first-order logic which may be a necessary extension for future versions of Zeno.

The three properties which Zeno was unable to prove from our test suite are those requiring lemmas which are not a generalisation of a sub-goal. We would like to investigate whether it is possible to develop a system which can prove \emph{any} property where all necessary sub-properties can be inferred through generalisation. In addition we would like to be able to prove some properties which are not in this set through intelligent methods to find these necessary lemmas. One such technique might be the random perturbation of property terms as in IsaCoSy\cite{isacosy}.

Finally, even though all Zeno proof steps correspond to axioms from classical logic, as further work 
we consider it important to construct a formal
 proof of the soundness of our method with respect to the operational semantics of \textbf{HC} along with a proof that our method of gradually constructing induction schemata does indeed preserve a well-founded ordering through usable induction hypotheses.

\begin{comment}

Even though all Zeno proof steps correspond to axioms from classical logic, as further work 
we consider it important to construct a formal
 proof of the soundness of our method with respect to the operational semantics of \textbf{HC} along with a proof that our method of gradually constructing induction schemata does indeed preserve a well-founded ordering through usable induction hypotheses.
 %
As a further extension, we would like to have a proof checker validate the Zeno generated proofs, in a similar manner to  IsaPlanner whose proofs  are checked by the proof assistant Isabelle. 


Another demanding addition will be the inclusion of primitive data types, 
such as 32-bit integers, (\li{Int}). 
% , which are very prevalent in real-world Haskell programs. 
%These have no natural representation as a recursive data type, 
%and the functions operating on them, such as \li{+} and \li{-}, have no natural 
%representation as a recursive function, so we are unable to reason about 
% these types using our current methods.
This would require Zeno to be able to handle background lemmas about these types, and to develop heuristics for guiding their application to prevent a combinatorial explosion. For that we may apply
or adapt techniques from rippling or SMT-solvers.
  
 Finally, we want to expand Zeno to allow it to prove more  properties.
 Namely, all the unproven properties  from Section \ref{sec:comparison} could have been proven  had Zeno found the appropriate auxiliary lemmas. We therefore need  more intelligent methods for discovering these lemmas. We could try randomly perturbating the goals to create new intermediate lemmas (as in generic algorithms), or try synthesising lemmas from functions definitions as described in \cite{isacosy}.



\end{comment}